Inference at * 1 1 
Iof proof for Lemma equiv rel functionality wrt iff:



1. T : Type
2. T' : Type
3. E : TT
4. E' : T'T'
5. T = T'
6. x, y:T. E(x,y)  E'(x,y)
  ((a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c)))
   ((a:T'. E'(a,a))
   & (a, b:T'. E'(a,b)  E'(b,a))
   & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c))) 

latex

 by InteriorProof ((RW (HigherC (HypC 6)) 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n
CollapseTHENA ((Au) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   ((a:T. E'(a,a))
C1:   & (a, b:T. E'(a,b)  E'(b,a))
C1:   & (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c)))
C1:    ((a:T'. E'(a,a))
C1:    & (a, b:T'. E'(a,b)  E'(b,a))
C1:    & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
C.

Definitions	x. t(x), P  Q, P  Q, P  Q, P & Q, t  T, x(s1,s2), x:A. B(x), , {T}, x(s)
Lemmas	implies functionality wrt iff, all functionality wrt iff, and functionality wrt iff, iff functionality wrt iff